w:World. FairFifo  (e:E. state_after(e)  x:Idvartype(loc(e);x)) 

latex

Definitions

t  T, P  Q, x:A. B(x), loc(e), vartype(i;x), x:AB(x), S  T, <a,b>, Id, s = t, E, w-pred(w;e), x.A(x), pred(e), val(e), Type, f(a), kindcase(k; a.f(a); l,t.g(l;t) ), V(i;k), w-machine(w;i), 2of(t), 1of(t), Knd, #$n, AB, a<b, Void, False, A, {x:A| B(x) }, , , s(i;t).x, w-info(w;e), pred!(e;e'), SWellFounded(R(x;y)), first(e), b, loc(e), S  T, state_after(e;info;pred?;init;Trans;val), state_after(e), World, FairFifo, w.T, w.TA, w.M, x:AB(x), w-automaton(T;TA;M), IdLnk, a(i;t), kind(a), x,y. t(x;y), x. t(x), act(e), kind(e), Prop, x:A. B(x), time(e)

Lemmas

w-time wf, pred! wf, nat wf, w-pred!-decreases, w-kind-lemma, subtype rel self, kindcase wf, w-kind wf, w-a wf, IdLnk wf, w-machine wf, w-automaton wf, fair-fifo wf, world wf, state after wf, w-TA wf, w-M wf, w-T wf, loc wf, Id wf, w-info wf, not wf, assert wf, first wf, w-s wf, le wf, w-eval wf, pred wf, w-pred wf, w-E wf, w-loc-lemma, w-vartype wf, w-loc wf, w-loc-pred